00100	AUTOMATIC SORTING
00200	
00300		This is a proposal for putting sorts into PCHECK.
00400	
00500	1. Sorts are attached to variables where variables are
00600	denoted by strings of letters only by declarations.  The
00700	sort attached to a letter string will automatically apply
00800	to any variables obtained from the given ones by suffixing
00900	digits.  This includes those generated by the routines
01000	that change bound variables in order to avoid capturing.
01100	
01200	2. Some constants such as S-expressions automatically have
01300	sorts.
01400	
01500	3. Not all variables have sorts.
01600	
01700	4. A variable is declared sorted by a command like
01800	
01900		DECLARE(X,(∀ Y)(P(X,Y,Z) ⊃ Q(X,Y)));
02000	
02100	Note that in this example Y is bound by a quantifier, Z is
02200	free, and X is the variable being declared.  The effect is
02300	to restrict the range over which X is quantified to individuals
02400	satisfying the predicate used.  A simpler and probably
02500	more common declaration is
02600	
02700		DECLARE(X, XεI0);
02800	
02900	which asserts that X is declared to be a non-negative integer.
03000	
03100	5. Suppose X has been declared to satisfy the predicate P.
03200	Then a sentence (∀ X)(e(X)) really means (∀ X)(P X ⊃ e(X)), and
03300	(∃ X)(e(X)) really means (∃ X)(P X ∧ e(X)).
03400	
03500	6. All the propositional calculus rules of the proof checker
03600	remain as before.  The universal and existential generalization
03700	and specialization rules remain the same when variables are
03800	replaced by or replace terms of the same sort.
03900	
04000	7. On the other hand, suppose universal specialization is to
04100	be applied to a formula (∀ N)(Q N) where N has been declared
04200	a non-negative integer by DECLARE(N,NεI0) as exemplified above and
04300	suppose that it is to be specialized to M where M has been
04400	declared and integer in general by DECLARE(M,MεI).  Then the
04500	effect of US(line,M) is to produce a formula
04600	
04700		MεI0 ⊃ Q(M).
04800	
04900	8. Now suppose we do UG(@,M,X) where X is an undeclared variable.
05000	Now the new line is
05100	
05200		(∀ X)(XεI⊃(XεI0⊃Q(X))).
05300	
05400	Using the fact that I0⊂I to simplify the formula is the user's
05500	responsibility.
05600	
05700	9. However, if X is undeclared and if we
05800	have the line  XεI0⊃P(X), then UG(@,X,N) gives (∀ N)(P(N)) if
05900	N has been declared to be in I0.
06000	
06100	10. The exact form of the rules remains to be worked out including
06200	the rules if any for handling replacement and λ-expressions.